| Definitions |  x:A. B(x), t  T, P   Q, i  j , A  B,  A, False,  , S  T, P  Q, P Q, P & Q, {i..j }, i j < k, SQType(T), {T},  T, True, P  Q, msgs(l;before(e')), as @ bs, rcvs(l;before(e')), Y, mapfilter(f;P;L), Top, filter(P;l), reduce(f;k;as), if b then t else f fi , tt, ff, map(f;as), emsg(e),  , A c B, (Msg on l),  x:A. B(x), ||as||, SqStable(P),  , Unit, Dec(P),  |
| Lemmas | event system wf, nat wf, nat properties, ge wf, length wf1, es-Msgl wf, es-lnk wf, es-snds-index wf, es-sender wf, es-index wf, int seg wf, es-sends wf, assert wf, es-isrcv wf, es-E wf, length zero, es-fifo-nil, es-Msg wf, not functionality wrt iff, last-es-snds-index, le wf, es-axioms, append wf, squash wf, true wf, IdLnk wf, select wf, length append, es-msgs wf, member-es-before, es-locl wf, es-before-decomp, mapfilter wf, es-haslnk wf, es-msg wf, sq stable from decidable, decidable assert, assert-es-haslnk, es-before wf, filter append, map append sq, filter wf, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, null wf3, top wf, assert of null, member exists, member map filter, length wf nat, es-before wf2, Id wf, es-loc wf, l before wf, member wf, append assoc sq, l before append, member append, cons member, l member wf, l before-es-before, or functionality wrt iff |
isrcv(e))